p:FinProbSpace, f:(), X:(n:RandomVariable(p;f(n))), N:, Z:RandomVariable(p;N), n:.
(i:{0..n}. f(i) < N)
 (i:{0..(n - 1)}. rv-disjoint(p;N;X(i);Z))
 (k:{0..n}. rv-disjoint(p;N;rv-partial-sum(k;i.X(i));Z)) 

latex

Definitions	x:A. B(x), , x(s), P  Q, {i..j}, t  T, i  j < k, P & Q, , Top, S  T, i  j , A  B, A, False, T, True, RandomVariable(p;n), rv-partial-sum(n;i.X(i)), rv-const(a), SQType(T), {T}, suptype(S; T), x. t(x), X + Y, P  Q, P  Q, FinProbSpace, Dec(P), P  Q
Lemmas	random-variable wf, nat wf, finite-prob-space wf, le wf, int seg wf, rv-disjoint wf, length wf nat, top wf, rationals wf, nat properties, ge wf, decidable int equal, rv-disjoint-const, int inc rationals, squash wf, true wf, int-rational, sum unroll base q, rv-disjoint-rv-add2, rv-partial-sum wf, qsum wf, subtype rel function, qadd wf, sum unroll hi q